r:CRng. IsField(r)  IsIntegDom(r) 

latex

Up	rings 1
Definitions	CRng, t  T, Rng, x:A. B(x), 1, a | b in r, 0, |r|, a  b  T , , P  Q, P & Q, A, *, x f y, IsIntegDom(r), IsField(r), P  Q, Dec(P), s = t, x:A  B(x), x:A. B(x), {x:A| B(x)} , False, x:AB(x), f(a), P  Q, P  Q, s ~ t, {T}, SQType(T), let x,y = A in B(x;y), t.1
Lemmas	rng times zero, rng times assoc, rng times one, decidable rng eq, rng times wf, not wf, nequal wf, rng car wf, rng zero wf, ring divs wf, rng one wf, crng wf